Nuprl Lemma : fun_thru_spread 2,24

A:Type, B:(AType), p:(x:AB(x)), CD:Type, f:(CD), b:(x:AB(x)C).
f(p/x,yb(x,y)) = (p/x,yf(b(x,y))) 
latex


Definitionsx:AB(x), x(s), t  T, x(s1,s2)

origin